Nuprl Lemma : cmseq?_wf
11,40
postcript
pdf
x
:chain_master(). cmseq?(
x
)
latex
Definitions
s
=
t
,
t
T
,
,
tt
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
Id
,
type
List
,
ff
,
,
x
.
A
(
x
)
,
x
,
y
,
z
.
t
(
x
;
y
;
z
)
,
x
.
t
(
x
)
,
case
x
of config(
list
) =>
config
(
list
) seq(
from
,
to
,
num
) =>
seq
(
from
;
to
;
num
)
,
chain_master()
,
cmseq?(
x
)
,
a
:
A
fp
B
(
a
)
,
strong-subtype(
A
;
B
)
,
P
Q
Lemmas
member
wf
,
chain
master
wf
,
chain
master
ind
wf
,
bool
wf
,
bfalse
wf
,
Id
wf
,
btrue
wf
,
nat
wf
origin
T, 
, tt, x:A
B(x), 
x:A. B(x), Id, type List, ff, 
, 
x.A(x), 
x,y,z. t(x;y;z), x. t(x), case x of config(list) => config(list) seq(from,to,num) => seq(from;to;num), chain_master(), cmseq?(x), a:A fp B(a), strong-subtype(A;B), P 
Q